$\forall$${\it es}$:ES, $P$:(E$\rightarrow\mathbb{P}$), $Q$, $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$), $f$:(\{$e$:E$\mid$ $P$($e$)\} $\rightarrow$E).
\\[0ex]Refl(E;$e$,${\it e'}$.$Q$($e$,${\it e'}$))
\\[0ex]$\Rightarrow$ AntiSym(E;$e$,${\it e'}$.$R$($e$,${\it e'}$))
\\[0ex]$\Rightarrow$ $f$ is $Q${-}$R${-}pre{-}preserving on $P$
\\[0ex]$\Rightarrow$ Inj(\{$e$:E$\mid$ $P$($e$)\} ;E;$f$)